\begin{tabbing}
case($R$)
\\[0ex]Rnone: ${\it none}$
\\[0ex]${\it left}$ $\oplus$ ${\it right}$: ${\it comb}$(${\it left}$;${\it right}$)
\\[0ex]base($b$). ${\it base}$($b$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ ${\it none}$
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.${\it comb}$(${\it rec}_{1}$;${\it rec}_{2}$)
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ ${\it base}$(Rinit(${\it loc}$;$T$;$x$;$v$))
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ ${\it base}$(Rframe(${\it loc}$;$T$;$x$;$L$))
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ ${\it base}$(Rsframe(${\it lnk}$;${\it tag}$;$L$))
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ ${\it base}$(Reffect(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$))
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ ${\it base}$(Rsends(${\it ds}$;${\it knd}$;$T$;$l$;${\it dt}$;$g$))
\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ ${\it base}$(Rpre(${\it loc}$;${\it ds}$;$a$;$T$;$P$))
\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ ${\it base}$(Raframe(${\it loc}$;$k$;$L$))
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ ${\it base}$(Rbframe(${\it loc}$;$k$;$L$))
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ ${\it base}$(Rrframe(${\it loc}$;$x$;$L$))
\-
\end{tabbing}